//  Copyright 2011 Charlie Garrett
//
//  Licensed under the Apache License, Version 2.0 (the "License");
//  you may not use this file except in compliance with the License.
//  You may obtain a copy of the License at
//
//  http://www.apache.org/licenses/LICENSE-2.0
//
//  Unless required by applicable law or agreed to in writing, software
//  distributed under the License is distributed on an "AS IS" BASIS,
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//  See the License for the specific language governing permissions and
//  limitations under the License.
//
//  Parser.cpp
//

// Our working Prolog-like grammar is:
//
// PROGRAM       ::= (CLAUSE | QUERY)*
// CLAUSE        ::= LITERAL CLAUSE_TAIL '.'
// QUERY         ::= '?-' LITERAL '.'
// LITERAL       ::= symbol PARAMETERS
// PARAMETERS    ::= empty | '(' ARGUMENTS ')'
// ARGUMENTS     ::= TERM (',' TERM)*
// TERM          ::= NUMERIC_TERM | SYMBOLIC_TERM | LIST
// NUMERIC_TERM  ::= number | '-' number
// SYMBOLIC_TERM ::= symbol | symbol '(' ARGUMENTS ')' | OPERATION '(' ARGUMENTS ')'
// OPERATION     ::= '+' | '-' | '*' | '/' | '==' | '\==' | '<' | '=<' | '>' | '>='
// CLAUSE_TAIL   ::= empty | ':-' LITERALS
// LITERALS      ::= LITERAL (',' LITERAL)*
// LIST          ::= '[' LIST_ARGS ']'
// LIST_ARGS     ::= empty | ARGUMENTS LIST_ARGS_END
// LIST_ARGS_END ::= empty | '|' TERM
// 

#include <map>
#include <vector>

#include <boost/smart_ptr/scoped_ptr.hpp>

#include "Lexeme.h"
#include "Parser.h"
#include "Term.h"

namespace logic {
    Parser::Parser(istream &in, bool tr) : input(in), cur_token(0, 0, ""), trace(tr) {
        Lexeme<istream::char_type>::ResetCounters();
        ConsumeToken();
    }

    // Consume the current token, skipping comments.
    bool Parser::ConsumeToken() {
        do {
            if (!(input >> cur_token)) {
                // Failed to consume one.
                return false;
            }
        } while (cur_token.IsKind(COMMENT));
        return true;
    }
    
    // Consume the current token only if it is the specified kind.
    bool Parser::ConsumeTokenOfKind(LexemeKind kind) {
        Trace("ConsumeTokenOfKind", kind);

        if (!cur_token.IsKind(kind)) {
            return false;
        }
        ConsumeToken();
        return true;
    }
    
    bool Parser::AtEOF() {
        return input.eof();
    }
    
    bool Parser::InputValid() {
        return !input.fail();
    }
    
    void Parser::Trace(const char *function) {
        if (trace) {
            cout << function << ": " << cur_token << endl;
        }
    }
    
    void Parser::Trace(const char *function, const LexemeKind kind) {
        if (trace) {
            cout << function << " with kind " << kind << ": " << cur_token << endl;
        }
    }
    
    // TODO:
    // Parse list notation
    // [], [L], [K, L, M], [Head|[Tail]], [Head|Tail] (done)
    // Allow compound goals.
    // Parse singly-quoted strings as constants
    // Parse doubly-quoted strings as lists? or as strings?
    // Parse infix operators
    // Parse cut (!)
    // Parse all punctuation (\, +, -, /, *, \+, ...)
    // Parse ()'s for tuples
    // Allow existentially quantified variables with ^?
    
    
    // Parses the input stream and returns a Prolog program if the input is legal
    // and NULL otherwise.
    // A program is a possibly empty sequence of clauses and queries.
    // PROGRAM ::= (CLAUSE | QUERY)*
    Program *Parser::ParseProgram() {
        Trace("ParseProgram");
        
        auto_ptr<Program> program(new Program());
        
        while (!AtEOF()) {
            Clause *clause = ParseClause();
            if (clause != NULL) {
                if (trace) {
                    cout << "Parsed clause: " << clause->ToString() << endl;
                }
                program->AddClause(clause);
            } else {
                // TODO:  Generalize queries to sequences of goals.
                Predicate *query = ParseQuery();
                if (query != NULL) {
                    if (trace) {
                        cout << "Parsed query: " << query->ToString() << endl;
                    }
                    program->AddQuery(query);
                } else {
                    cout << "Parsing failure at " << cur_token << endl;
                    break;
                }
            }
        }
        
        if (AtEOF()) {
            return program.release();
        } else {
            // Could not read the whole input.
            return NULL;
        }
    }
    
    // Parses the input stream and returns a Clause if the data is syntactically legal
    // and NULL otherwise.
    // A clause is either a fact (a literal followed by a period) or a rule
    // (a literal followed by :-, a body and a period)
    // CLAUSE ::= LITERAL CLAUSE_TAIL '.'
    Clause *Parser::ParseClause() {
        Trace("ParseClause");
        
        variables.clear();
        auto_ptr<Predicate> head(ParseLiteral());
        if (head.get() == NULL) {
            return NULL;
        }

        auto_ptr<vector<Predicate*> > body(ParseClauseTail());
        if (body.get() == NULL) {
            return NULL;
        }
        
        if (!ConsumeTokenOfKind(PERIOD)) {
            for (vector<Predicate*>::iterator b = body->begin(); b != body->end(); ++b) {
                delete (*b);
            }
            return NULL;
        }
        
        return new Clause(head.release(), *body);
    }
    
    // Parses the input stream and returns a Predicate if the input is syntactically legal
    // and NULL otherwise.
    // A literal is a symbol followed by a parameter list.
    // LITERAL ::= symbol PARAMETERS
    Predicate *Parser::ParseLiteral() {
        Trace("ParseLiteral");
        
        string name;
        if (cur_token.IsKind(SYMBOL)) {
            name = cur_token.GetText();
            ConsumeToken();
        } else {
            return NULL;
        }

        auto_ptr<vector<Term*> > terms(ParseParameters());
        if (terms.get() == NULL) {
            return NULL;
        }
        
        return new Predicate(name, *terms);
    }

    // Parses the input stream and returns a query Predicate if the input is
    // syntactically legal and NULL otherwise.
    // A query is a '?-' token followed by a literal and a period.
    // QUERY ::= '?-' LITERAL '.'
    Predicate *Parser::ParseQuery() {
        Trace("ParseQuery");
        
        variables.clear();
        if (!ConsumeTokenOfKind(QUERY)) {
            return NULL;
        }

        auto_ptr<Predicate> query(ParseLiteral());
        if (query.get() == NULL) {
            return NULL;
        }
        
        if (ConsumeTokenOfKind(PERIOD)) {
            return query.release();
        } else {
            return NULL;
        }
    }

    // Parses the input stream and returns a vector of Terms if the input is
    // syntactically legal and NULL otherwise.
    // A parameter list either empty, or a parenthesized sequence of arguments.
    // PARAMETERS ::= empty | '(' ARGUMENTS ')'
    vector<Term*> *Parser::ParseParameters() {
        Trace("ParseParameters");
        
        if (!ConsumeTokenOfKind(OPEN_PAREN)) {
            // An empty list.
            return new vector<Term*>();
        }
        auto_ptr<vector<Term*> > args(ParseArguments());
        if (args.get() == NULL) {
            return NULL;
        }
        if (!ConsumeTokenOfKind(CLOSE_PAREN)) {
            for (vector<Term*>::iterator a = args->begin(); a != args->end(); ++a) {
                delete (*a);
            }
            return NULL;
        } else {
            return args.release();
        }
    }
    
    // Parses the input stream and returns a vector of Terms if the input is
    // syntactically legal and NULL otherwise.
    // An argument list is a comma-separated list of at least one term.
    // ARGUMENTS ::= TERM (',' TERM)*
    vector<Term*> *Parser::ParseArguments() {
        Trace("ParseArguments");

        Term *t = ParseTerm();
        if (t == NULL) {
            return NULL;
        }

        auto_ptr<vector<Term*> > args(new vector<Term*>(1, t));
        while (ConsumeTokenOfKind(COMMA)) {
            t = ParseTerm();
            if (t == NULL) {
                for (vector<Term*>::iterator a = args->begin(); a != args->end(); ++a) {
                    delete (*a);
                }
                return NULL;
            } else {
                args->push_back(t);
            }
        }
        return args.release();
    }
    
    // Parses the input stream and returns a Term if the input is
    // syntactically legal and NULL otherwise.
    // A term is a number, or a symbol token, optionally followed
    // by a parenthesized argument list, or a bracketed list of terms.
    // Both numeric terms and symbolic terms have productions starting
    // with '-'.  Disambiguate them here.
    // TERM ::= NUMERIC_TERM | SYMBOLIC_TERM | LIST
    Term *Parser::ParseTerm() {
        Trace("ParseTerm");

        bool have_minus = cur_token.IsKind(MINUS);
        if (have_minus) {
            ConsumeToken();
        }
        
        Term *term = ParseNumericTerm(have_minus);
        if (term != NULL) {
            return term;
        }
        
        term = ParseSymbolicTerm(have_minus);
        if (term != NULL) {
            return term;
        }
        
        // If it's not a list, then it's illegal.
        return ParseList();
    }
    
    // Parses the input stream and returns a Term if the input is
    // syntactically legal and NULL otherwise.
    // A numeric term is a number, optionally preceded by a unary minus sign,
    // but the minus sign will have been read by the caller and its presence
    // is indicated by the have_minus argument.
    // NUMERIC_TERM  ::= number | '-' number
    Term *Parser::ParseNumericTerm(bool have_minus) {
        Trace("ParseNumericTerm");
        
        if (cur_token.IsKind(NUMBER)) {
            double value;
            istringstream is(cur_token.GetText());
            if (is >> value) {
                ConsumeToken();
                if (have_minus) {
                    return new Constant(-value);
                } else {
                    return new Constant(value);
                }
            }
        }
        return NULL;
    }
    // SYMBOLIC_TERM ::= symbol | symbol '(' ARGUMENTS ')' | OPERATION '(' ARGUMENTS ')'
    Term *Parser::ParseSymbolicTerm(bool have_minus) {
        Trace("ParseSymbolicTerm");
        
        // TODO:  Continue rewrite from here.
        // Add call to ParseOperation.  Account for previously parsed minus signs.
        
        bool is_quoted = false;
        bool is_op = false;
        string name;
        if (have_minus) {
            name = "-";
            is_op = true;
        } else {
            is_quoted = cur_token.IsKind(SINGLY_QUOTED_STRING);
            if (is_quoted || cur_token.IsKind(SYMBOL)) {
                name = cur_token.GetText();
                ConsumeToken();
            } else {
                name = ParseOperation();
                if (name.empty()) {
                    return NULL;
                }
                is_op = true;
            }
        }
        
        if (!ConsumeTokenOfKind(OPEN_PAREN)) {
            // The term is a Constant if it begins with a lowercase letter and
            // a Variable if it begins with an uppercase letter and illegal if
            // it begins with a number.
            const char initial = name.at(0);
            if (is_quoted || islower(initial) || isnumber(initial)) {
                return new Constant(name);
            } else if (isupper(initial) || initial == '_') {
                if (variables.find(name) == variables.end()) {
                    variables[name] = new Variable(name);
                }
                return variables[name];
            } else {
                return NULL;
            }
        }
        
        auto_ptr<vector<Term*> > args(ParseArguments());
        if (args.get() == NULL) {
            return NULL;
        }
        if (!ConsumeTokenOfKind(CLOSE_PAREN) ||
            (is_op && args->size() != 2)) {
            for (vector<Term*>::iterator a = args->begin(); a != args->end(); ++a) {
                delete (*a);
            }
            return NULL;
        } else {
            return new Structure(name, *args);
        }        
    }
    
    // Parses the input stream and returns a string containing an
    // operation if the input is syntactically legal or an empty
    // string otherwise.
    // Minus signs should be consumed by callers, so they are disallowed
    // by this method.
    // OPERATION     ::= '+' | '-' | '*' | '/' | '==' | '\==' | '<' | '=<' | '>' | '>='
    string Parser::ParseOperation() {
        Trace("ParseOperation");
        
        switch (cur_token.GetKind()) {
            case PLUS:
            case TIMES:
            case DIVIDE:
            case EQUAL:
            case NOT_EQUAL:
            case LESS_THAN:
            case LESS_OR_EQUAL:
            case GREATER_THAN:
            case GREATER_OR_EQUAL: {
                string name = cur_token.GetText();
                ConsumeToken();
                return name;
            }
            default:
                return "";
        }
    }
    
    
    // Parses the input stream and returns a vector of Predicates if the input is
    // syntactically legal and NULL otherwise.
    // A clause tail is either empty or :-, and a body.
    // CLAUSE_TAIL ::= empty | ':-' LITERALS
    vector<Predicate*> *Parser::ParseClauseTail() {
        Trace("ParseClauseTail");

        if (!ConsumeTokenOfKind(IMPLICATION)) {
            // An empty clause tail.
            return new vector<Predicate*>();
        }
        return ParseLiterals();
    }
    
    // Parses the input stream and returns a vector of Predicates if the input is
    // syntactically legal and NULL otherwise.
    // A literal list is a comma-separated list of at least one literal.
    // LITERALS ::= LITERAL (',' LITERAL)*
    vector<Predicate*> *Parser::ParseLiterals() {
        Trace("ParseLiterals");

        Predicate *p = ParseLiteral();
        if (p == NULL) {
            return NULL;
        }

        auto_ptr<vector<Predicate*> > lits(new vector<Predicate*>(1, p));
        while (ConsumeTokenOfKind(COMMA)) {
            p = ParseLiteral();
            if (p == NULL) {
                for (vector<Predicate*>::iterator lit = lits->begin(); lit != lits->end(); ++lit) {
                    delete (*lit);
                }
            } else {
                lits->push_back(p);
            }
        }
        return lits.release();
    }
    
    // Parses a list in []'s and returns a Structure with Functor ListCons if
    // the input is syntactically legal and NULL otherwise.
    // A list is a comma-separated sequence of terms, possibly empty or possibly
    // ending in "| term", contained within square brackets.
    // LIST ::= '[' LIST_ARGS ']'
    Term *Parser::ParseList() {
        Trace("ParseList");
        
        if (!ConsumeTokenOfKind(OPEN_SQUARE_BRACKET)) {
            // Not a list
            return NULL;
        }
        
        auto_ptr<Term> list(ParseListArgs());
        if (list.get() == NULL) {
            return NULL;
        }
        
        if (!ConsumeTokenOfKind(CLOSE_SQUARE_BRACKET)) {
            // Not a list
            return NULL;
        }
        
        return list.release();
    }
    
    // Parses the arguments of a list and returns a Structure with Functor EmptyList or
    // or ListCons if the input is syntactically legal and NULL otherwise.
    // List arguments are a comma-separated sequence of terms, possibly empty or
    // possibly ending in '| term'.
    // LIST_ARGS ::= empty | ARGUMENTS LIST_ARGS_END
    Term *Parser::ParseListArgs() {
        Trace("ParseListArgs");
        
        if (cur_token.IsKind(CLOSE_SQUARE_BRACKET)) {
            // An empty argument list.
            return new EmptyListConstant();
        }
        
        auto_ptr<vector<Term*> >initial_args(ParseArguments());
        if (initial_args.get() == NULL) {
            return NULL;
        }
        
        auto_ptr<vector<Term*> >final_arg(ParseListArgsEnd());
        if (final_arg.get() == NULL) {
            for (vector<Term*>::iterator ia = initial_args->begin();
                 ia != initial_args->end(); ++ia) {
                delete (*ia);
            }
            return NULL;
        }
                
        if (final_arg->size() != 0) {
            assert(final_arg->size() == 1);
            if (initial_args->size() == 0) {
                // [ | term] is not legal.  There must be some initial args.
                return NULL;
            }
        }

        // Build a tree of structures to represent the list.
        vector<Term*> no_args;
        Term *list = (final_arg->size() == 0 ? new EmptyListConstant()
                                             : final_arg->at(0));

        for (long n = initial_args->size() - 1; n >= 0; n--) {
            vector<Term*> cons_args;
            cons_args.push_back(initial_args->at(n));
            cons_args.push_back(list);
            list = new ListConsStructure(cons_args);
        }
        return list;
    }
    
    // Parses the tail end of the arguments of a list and returns a vector of 0 or 1
    // Terms if the input is syntactically legal and NULL otherwise.
    // The end of list arguments are either empty or '|' followed by a single term.
    // LIST_ARGS_END ::= empty | '|' TERM
    vector<Term*> *Parser::ParseListArgsEnd() {
        Trace("ParseListArgsEnd");
        
        if (!ConsumeTokenOfKind(LIST_CONS)) {
            // An empty end of list arguments.
            return new vector<Term*>();
        }
        
        Term *t = ParseTerm();
        if (t == NULL) {
            // Syntactically invalid term.
            return NULL;
        } else {
            // A valid end of list arguments with one term.
            return new vector<Term*>(1, t);
        }
    }
}  // namespace logic
